\begin{tabbing}
(\%S\% 
\\[0ex]$\backslash$p.\=let x = get\_distinct\_var `x' p \+
\\[0ex]in let n = get\_var\_arg `n` p 
\\[0ex]
\\[0ex]in let S = get\_term\_arg `S` p 
\\[0ex]in let T = get\_term\_arg `T` p 
\\[0ex]
\\[0ex]in let f = get\_term\_arg `f` p 
\\[0ex]in 
\\[0ex]As\=sert \+
\\[0ex](m\=k\_all\_term x T \+
\\[0ex](
\-\-\-\\[0ex]mk\_all\_te\=rm n S \+
\\[0ex](mk\=\_implies\_term \+
\\[0ex](mk\_equal\_term T (mk\_apply\_term f 
\-\-\\[0ex](mvt n)) (mv\=t x)) \+
\\[0ex](concl p)))) p)
\-
\end{tabbing}